The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(n^1, INF).

0 CpxTRS
↳1 DecreasingLoopProof (⇔, 390 ms)
↳2 BOUNDS(n^1, INF)
↳3 RenamingProof (⇔, 0 ms)
↳4 CpxRelTRS
    ↳5 TypeInferenceProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳6 typed CpxTrs
    ↳7 OrderProof (LOWER BOUND(ID), 0 ms)
    ↳8 typed CpxTrs
    ↳9 NoRewriteLemmaProof (LOWER BOUND(ID), 2273 ms)
    ↳10 typed CpxTrs
    ↳11 NoRewriteLemmaProof (LOWER BOUND(ID), 415 ms)
    ↳12 typed CpxTrs
    ↳13 NoRewriteLemmaProof (LOWER BOUND(ID), 395 ms)
    ↳14 typed CpxTrs
    ↳15 NoRewriteLemmaProof (LOWER BOUND(ID), 384 ms)
    ↳16 typed CpxTrs
    ↳17 NoRewriteLemmaProof (LOWER BOUND(ID), 957 ms)
    ↳18 typed CpxTrs
    ↳19 NoRewriteLemmaProof (LOWER BOUND(ID), 1449 ms)
    ↳20 typed CpxTrs
    ↳21 NoRewriteLemmaProof (LOWER BOUND(ID), 1298 ms)
    ↳22 typed CpxTrs

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

f4(S(x''), S(x'), x3, x4, S(x)) → f2(S(x''), x', x3, x4, x)
f4(S(x'), 0, x3, x4, S(x)) → f3(x', 0, x3, x4, x)
f2(x1, x2, S(x''), S(x'), S(x)) → f5(x1, x2, S(x''), x', x)
f2(x1, x2, S(x'), 0, S(x)) → f3(x1, x2, x', 0, x)
f4(S(x'), S(x), x3, x4, 0) → 0
f4(S(x), 0, x3, x4, 0) → 0
f2(x1, x2, S(x'), S(x), 0) → 0
f2(x1, x2, S(x), 0, 0) → 0
f0(x1, S(x'), x3, S(x), x5) → f1(x', S(x'), x, S(x), S(x))
f0(x1, S(x), x3, 0, x5) → 0
f6(x1, x2, x3, x4, S(x)) → f0(x1, x2, x4, x3, x)
f5(x1, x2, x3, x4, S(x)) → f6(x2, x1, x3, x4, x)
f3(x1, x2, x3, x4, S(x)) → f4(x1, x2, x4, x3, x)
f1(x1, x2, x3, x4, S(x)) → f2(x2, x1, x3, x4, x)
f6(x1, x2, x3, x4, 0) → 0
f5(x1, x2, x3, x4, 0) → 0
f4(0, x2, x3, x4, x5) → 0
f3(x1, x2, x3, x4, 0) → 0
f2(x1, x2, 0, x4, x5) → 0
f1(x1, x2, x3, x4, 0) → 0
f0(x1, 0, x3, x4, x5) → 0

Rewrite Strategy: INNERMOST

(1) DecreasingLoopProof (EQUIVALENT transformation)

The following loop(s) give(s) rise to the lower bound Ω(n1):
The rewrite sequence
f4(S(x'), 0, x3, x4, S(S(x20081_7))) →+ f4(x', 0, x4, x3, x20081_7)
gives rise to a decreasing loop by considering the right hand sides subterm at position [].
The pumping substitution is [x' / S(x'), x20081_7 / S(S(x20081_7))].
The result substitution is [x3 / x4, x4 / x3].

(2) BOUNDS(n^1, INF)

(3) RenamingProof (EQUIVALENT transformation)

Renamed function symbols to avoid clashes with predefined symbol.

(4) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

f4(S(x''), S(x'), x3, x4, S(x)) → f2(S(x''), x', x3, x4, x)
f4(S(x'), 0', x3, x4, S(x)) → f3(x', 0', x3, x4, x)
f2(x1, x2, S(x''), S(x'), S(x)) → f5(x1, x2, S(x''), x', x)
f2(x1, x2, S(x'), 0', S(x)) → f3(x1, x2, x', 0', x)
f4(S(x'), S(x), x3, x4, 0') → 0'
f4(S(x), 0', x3, x4, 0') → 0'
f2(x1, x2, S(x'), S(x), 0') → 0'
f2(x1, x2, S(x), 0', 0') → 0'
f0(x1, S(x'), x3, S(x), x5) → f1(x', S(x'), x, S(x), S(x))
f0(x1, S(x), x3, 0', x5) → 0'
f6(x1, x2, x3, x4, S(x)) → f0(x1, x2, x4, x3, x)
f5(x1, x2, x3, x4, S(x)) → f6(x2, x1, x3, x4, x)
f3(x1, x2, x3, x4, S(x)) → f4(x1, x2, x4, x3, x)
f1(x1, x2, x3, x4, S(x)) → f2(x2, x1, x3, x4, x)
f6(x1, x2, x3, x4, 0') → 0'
f5(x1, x2, x3, x4, 0') → 0'
f4(0', x2, x3, x4, x5) → 0'
f3(x1, x2, x3, x4, 0') → 0'
f2(x1, x2, 0', x4, x5) → 0'
f1(x1, x2, x3, x4, 0') → 0'
f0(x1, 0', x3, x4, x5) → 0'

S is empty.
Rewrite Strategy: INNERMOST

(5) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(6) Obligation:

Innermost TRS:
Rules:
f4(S(x''), S(x'), x3, x4, S(x)) → f2(S(x''), x', x3, x4, x)
f4(S(x'), 0', x3, x4, S(x)) → f3(x', 0', x3, x4, x)
f2(x1, x2, S(x''), S(x'), S(x)) → f5(x1, x2, S(x''), x', x)
f2(x1, x2, S(x'), 0', S(x)) → f3(x1, x2, x', 0', x)
f4(S(x'), S(x), x3, x4, 0') → 0'
f4(S(x), 0', x3, x4, 0') → 0'
f2(x1, x2, S(x'), S(x), 0') → 0'
f2(x1, x2, S(x), 0', 0') → 0'
f0(x1, S(x'), x3, S(x), x5) → f1(x', S(x'), x, S(x), S(x))
f0(x1, S(x), x3, 0', x5) → 0'
f6(x1, x2, x3, x4, S(x)) → f0(x1, x2, x4, x3, x)
f5(x1, x2, x3, x4, S(x)) → f6(x2, x1, x3, x4, x)
f3(x1, x2, x3, x4, S(x)) → f4(x1, x2, x4, x3, x)
f1(x1, x2, x3, x4, S(x)) → f2(x2, x1, x3, x4, x)
f6(x1, x2, x3, x4, 0') → 0'
f5(x1, x2, x3, x4, 0') → 0'
f4(0', x2, x3, x4, x5) → 0'
f3(x1, x2, x3, x4, 0') → 0'
f2(x1, x2, 0', x4, x5) → 0'
f1(x1, x2, x3, x4, 0') → 0'
f0(x1, 0', x3, x4, x5) → 0'

Types:
f4 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
S :: S:0' → S:0'
f2 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
0' :: S:0'
f3 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
f5 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
f0 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
f1 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
f6 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
hole_S:0'1_7 :: S:0'
gen_S:0'2_7 :: Nat → S:0'

(7) OrderProof (LOWER BOUND(ID) transformation)

Heuristically decided to analyse the following defined symbols:
f4, f2, f3, f5, f0, f1, f6

They will be analysed ascendingly in the following order:
f4 = f2
f4 = f3
f4 = f5
f4 = f0
f4 = f1
f4 = f6
f2 = f3
f2 = f5
f2 = f0
f2 = f1
f2 = f6
f3 = f5
f3 = f0
f3 = f1
f3 = f6
f5 = f0
f5 = f1
f5 = f6
f0 = f1
f0 = f6
f1 = f6

(8) Obligation:

Innermost TRS:
Rules:
f4(S(x''), S(x'), x3, x4, S(x)) → f2(S(x''), x', x3, x4, x)
f4(S(x'), 0', x3, x4, S(x)) → f3(x', 0', x3, x4, x)
f2(x1, x2, S(x''), S(x'), S(x)) → f5(x1, x2, S(x''), x', x)
f2(x1, x2, S(x'), 0', S(x)) → f3(x1, x2, x', 0', x)
f4(S(x'), S(x), x3, x4, 0') → 0'
f4(S(x), 0', x3, x4, 0') → 0'
f2(x1, x2, S(x'), S(x), 0') → 0'
f2(x1, x2, S(x), 0', 0') → 0'
f0(x1, S(x'), x3, S(x), x5) → f1(x', S(x'), x, S(x), S(x))
f0(x1, S(x), x3, 0', x5) → 0'
f6(x1, x2, x3, x4, S(x)) → f0(x1, x2, x4, x3, x)
f5(x1, x2, x3, x4, S(x)) → f6(x2, x1, x3, x4, x)
f3(x1, x2, x3, x4, S(x)) → f4(x1, x2, x4, x3, x)
f1(x1, x2, x3, x4, S(x)) → f2(x2, x1, x3, x4, x)
f6(x1, x2, x3, x4, 0') → 0'
f5(x1, x2, x3, x4, 0') → 0'
f4(0', x2, x3, x4, x5) → 0'
f3(x1, x2, x3, x4, 0') → 0'
f2(x1, x2, 0', x4, x5) → 0'
f1(x1, x2, x3, x4, 0') → 0'
f0(x1, 0', x3, x4, x5) → 0'

Types:
f4 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
S :: S:0' → S:0'
f2 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
0' :: S:0'
f3 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
f5 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
f0 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
f1 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
f6 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
hole_S:0'1_7 :: S:0'
gen_S:0'2_7 :: Nat → S:0'

Generator Equations:
gen_S:0'2_7(0) ⇔ 0'
gen_S:0'2_7(+(x, 1)) ⇔ S(gen_S:0'2_7(x))

The following defined symbols remain to be analysed:
f2, f4, f3, f5, f0, f1, f6

They will be analysed ascendingly in the following order:
f4 = f2
f4 = f3
f4 = f5
f4 = f0
f4 = f1
f4 = f6
f2 = f3
f2 = f5
f2 = f0
f2 = f1
f2 = f6
f3 = f5
f3 = f0
f3 = f1
f3 = f6
f5 = f0
f5 = f1
f5 = f6
f0 = f1
f0 = f6
f1 = f6

(9) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol f2.

(10) Obligation:

Innermost TRS:
Rules:
f4(S(x''), S(x'), x3, x4, S(x)) → f2(S(x''), x', x3, x4, x)
f4(S(x'), 0', x3, x4, S(x)) → f3(x', 0', x3, x4, x)
f2(x1, x2, S(x''), S(x'), S(x)) → f5(x1, x2, S(x''), x', x)
f2(x1, x2, S(x'), 0', S(x)) → f3(x1, x2, x', 0', x)
f4(S(x'), S(x), x3, x4, 0') → 0'
f4(S(x), 0', x3, x4, 0') → 0'
f2(x1, x2, S(x'), S(x), 0') → 0'
f2(x1, x2, S(x), 0', 0') → 0'
f0(x1, S(x'), x3, S(x), x5) → f1(x', S(x'), x, S(x), S(x))
f0(x1, S(x), x3, 0', x5) → 0'
f6(x1, x2, x3, x4, S(x)) → f0(x1, x2, x4, x3, x)
f5(x1, x2, x3, x4, S(x)) → f6(x2, x1, x3, x4, x)
f3(x1, x2, x3, x4, S(x)) → f4(x1, x2, x4, x3, x)
f1(x1, x2, x3, x4, S(x)) → f2(x2, x1, x3, x4, x)
f6(x1, x2, x3, x4, 0') → 0'
f5(x1, x2, x3, x4, 0') → 0'
f4(0', x2, x3, x4, x5) → 0'
f3(x1, x2, x3, x4, 0') → 0'
f2(x1, x2, 0', x4, x5) → 0'
f1(x1, x2, x3, x4, 0') → 0'
f0(x1, 0', x3, x4, x5) → 0'

Types:
f4 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
S :: S:0' → S:0'
f2 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
0' :: S:0'
f3 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
f5 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
f0 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
f1 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
f6 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
hole_S:0'1_7 :: S:0'
gen_S:0'2_7 :: Nat → S:0'

Generator Equations:
gen_S:0'2_7(0) ⇔ 0'
gen_S:0'2_7(+(x, 1)) ⇔ S(gen_S:0'2_7(x))

The following defined symbols remain to be analysed:
f5, f4, f3, f0, f1, f6

They will be analysed ascendingly in the following order:
f4 = f2
f4 = f3
f4 = f5
f4 = f0
f4 = f1
f4 = f6
f2 = f3
f2 = f5
f2 = f0
f2 = f1
f2 = f6
f3 = f5
f3 = f0
f3 = f1
f3 = f6
f5 = f0
f5 = f1
f5 = f6
f0 = f1
f0 = f6
f1 = f6

(11) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol f5.

(12) Obligation:

Innermost TRS:
Rules:
f4(S(x''), S(x'), x3, x4, S(x)) → f2(S(x''), x', x3, x4, x)
f4(S(x'), 0', x3, x4, S(x)) → f3(x', 0', x3, x4, x)
f2(x1, x2, S(x''), S(x'), S(x)) → f5(x1, x2, S(x''), x', x)
f2(x1, x2, S(x'), 0', S(x)) → f3(x1, x2, x', 0', x)
f4(S(x'), S(x), x3, x4, 0') → 0'
f4(S(x), 0', x3, x4, 0') → 0'
f2(x1, x2, S(x'), S(x), 0') → 0'
f2(x1, x2, S(x), 0', 0') → 0'
f0(x1, S(x'), x3, S(x), x5) → f1(x', S(x'), x, S(x), S(x))
f0(x1, S(x), x3, 0', x5) → 0'
f6(x1, x2, x3, x4, S(x)) → f0(x1, x2, x4, x3, x)
f5(x1, x2, x3, x4, S(x)) → f6(x2, x1, x3, x4, x)
f3(x1, x2, x3, x4, S(x)) → f4(x1, x2, x4, x3, x)
f1(x1, x2, x3, x4, S(x)) → f2(x2, x1, x3, x4, x)
f6(x1, x2, x3, x4, 0') → 0'
f5(x1, x2, x3, x4, 0') → 0'
f4(0', x2, x3, x4, x5) → 0'
f3(x1, x2, x3, x4, 0') → 0'
f2(x1, x2, 0', x4, x5) → 0'
f1(x1, x2, x3, x4, 0') → 0'
f0(x1, 0', x3, x4, x5) → 0'

Types:
f4 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
S :: S:0' → S:0'
f2 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
0' :: S:0'
f3 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
f5 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
f0 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
f1 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
f6 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
hole_S:0'1_7 :: S:0'
gen_S:0'2_7 :: Nat → S:0'

Generator Equations:
gen_S:0'2_7(0) ⇔ 0'
gen_S:0'2_7(+(x, 1)) ⇔ S(gen_S:0'2_7(x))

The following defined symbols remain to be analysed:
f6, f4, f3, f0, f1

They will be analysed ascendingly in the following order:
f4 = f2
f4 = f3
f4 = f5
f4 = f0
f4 = f1
f4 = f6
f2 = f3
f2 = f5
f2 = f0
f2 = f1
f2 = f6
f3 = f5
f3 = f0
f3 = f1
f3 = f6
f5 = f0
f5 = f1
f5 = f6
f0 = f1
f0 = f6
f1 = f6

(13) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol f6.

(14) Obligation:

Innermost TRS:
Rules:
f4(S(x''), S(x'), x3, x4, S(x)) → f2(S(x''), x', x3, x4, x)
f4(S(x'), 0', x3, x4, S(x)) → f3(x', 0', x3, x4, x)
f2(x1, x2, S(x''), S(x'), S(x)) → f5(x1, x2, S(x''), x', x)
f2(x1, x2, S(x'), 0', S(x)) → f3(x1, x2, x', 0', x)
f4(S(x'), S(x), x3, x4, 0') → 0'
f4(S(x), 0', x3, x4, 0') → 0'
f2(x1, x2, S(x'), S(x), 0') → 0'
f2(x1, x2, S(x), 0', 0') → 0'
f0(x1, S(x'), x3, S(x), x5) → f1(x', S(x'), x, S(x), S(x))
f0(x1, S(x), x3, 0', x5) → 0'
f6(x1, x2, x3, x4, S(x)) → f0(x1, x2, x4, x3, x)
f5(x1, x2, x3, x4, S(x)) → f6(x2, x1, x3, x4, x)
f3(x1, x2, x3, x4, S(x)) → f4(x1, x2, x4, x3, x)
f1(x1, x2, x3, x4, S(x)) → f2(x2, x1, x3, x4, x)
f6(x1, x2, x3, x4, 0') → 0'
f5(x1, x2, x3, x4, 0') → 0'
f4(0', x2, x3, x4, x5) → 0'
f3(x1, x2, x3, x4, 0') → 0'
f2(x1, x2, 0', x4, x5) → 0'
f1(x1, x2, x3, x4, 0') → 0'
f0(x1, 0', x3, x4, x5) → 0'

Types:
f4 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
S :: S:0' → S:0'
f2 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
0' :: S:0'
f3 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
f5 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
f0 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
f1 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
f6 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
hole_S:0'1_7 :: S:0'
gen_S:0'2_7 :: Nat → S:0'

Generator Equations:
gen_S:0'2_7(0) ⇔ 0'
gen_S:0'2_7(+(x, 1)) ⇔ S(gen_S:0'2_7(x))

The following defined symbols remain to be analysed:
f0, f4, f3, f1

They will be analysed ascendingly in the following order:
f4 = f2
f4 = f3
f4 = f5
f4 = f0
f4 = f1
f4 = f6
f2 = f3
f2 = f5
f2 = f0
f2 = f1
f2 = f6
f3 = f5
f3 = f0
f3 = f1
f3 = f6
f5 = f0
f5 = f1
f5 = f6
f0 = f1
f0 = f6
f1 = f6

(15) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol f0.

(16) Obligation:

Innermost TRS:
Rules:
f4(S(x''), S(x'), x3, x4, S(x)) → f2(S(x''), x', x3, x4, x)
f4(S(x'), 0', x3, x4, S(x)) → f3(x', 0', x3, x4, x)
f2(x1, x2, S(x''), S(x'), S(x)) → f5(x1, x2, S(x''), x', x)
f2(x1, x2, S(x'), 0', S(x)) → f3(x1, x2, x', 0', x)
f4(S(x'), S(x), x3, x4, 0') → 0'
f4(S(x), 0', x3, x4, 0') → 0'
f2(x1, x2, S(x'), S(x), 0') → 0'
f2(x1, x2, S(x), 0', 0') → 0'
f0(x1, S(x'), x3, S(x), x5) → f1(x', S(x'), x, S(x), S(x))
f0(x1, S(x), x3, 0', x5) → 0'
f6(x1, x2, x3, x4, S(x)) → f0(x1, x2, x4, x3, x)
f5(x1, x2, x3, x4, S(x)) → f6(x2, x1, x3, x4, x)
f3(x1, x2, x3, x4, S(x)) → f4(x1, x2, x4, x3, x)
f1(x1, x2, x3, x4, S(x)) → f2(x2, x1, x3, x4, x)
f6(x1, x2, x3, x4, 0') → 0'
f5(x1, x2, x3, x4, 0') → 0'
f4(0', x2, x3, x4, x5) → 0'
f3(x1, x2, x3, x4, 0') → 0'
f2(x1, x2, 0', x4, x5) → 0'
f1(x1, x2, x3, x4, 0') → 0'
f0(x1, 0', x3, x4, x5) → 0'

Types:
f4 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
S :: S:0' → S:0'
f2 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
0' :: S:0'
f3 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
f5 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
f0 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
f1 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
f6 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
hole_S:0'1_7 :: S:0'
gen_S:0'2_7 :: Nat → S:0'

Generator Equations:
gen_S:0'2_7(0) ⇔ 0'
gen_S:0'2_7(+(x, 1)) ⇔ S(gen_S:0'2_7(x))

The following defined symbols remain to be analysed:
f1, f4, f3

They will be analysed ascendingly in the following order:
f4 = f2
f4 = f3
f4 = f5
f4 = f0
f4 = f1
f4 = f6
f2 = f3
f2 = f5
f2 = f0
f2 = f1
f2 = f6
f3 = f5
f3 = f0
f3 = f1
f3 = f6
f5 = f0
f5 = f1
f5 = f6
f0 = f1
f0 = f6
f1 = f6

(17) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol f1.

(18) Obligation:

Innermost TRS:
Rules:
f4(S(x''), S(x'), x3, x4, S(x)) → f2(S(x''), x', x3, x4, x)
f4(S(x'), 0', x3, x4, S(x)) → f3(x', 0', x3, x4, x)
f2(x1, x2, S(x''), S(x'), S(x)) → f5(x1, x2, S(x''), x', x)
f2(x1, x2, S(x'), 0', S(x)) → f3(x1, x2, x', 0', x)
f4(S(x'), S(x), x3, x4, 0') → 0'
f4(S(x), 0', x3, x4, 0') → 0'
f2(x1, x2, S(x'), S(x), 0') → 0'
f2(x1, x2, S(x), 0', 0') → 0'
f0(x1, S(x'), x3, S(x), x5) → f1(x', S(x'), x, S(x), S(x))
f0(x1, S(x), x3, 0', x5) → 0'
f6(x1, x2, x3, x4, S(x)) → f0(x1, x2, x4, x3, x)
f5(x1, x2, x3, x4, S(x)) → f6(x2, x1, x3, x4, x)
f3(x1, x2, x3, x4, S(x)) → f4(x1, x2, x4, x3, x)
f1(x1, x2, x3, x4, S(x)) → f2(x2, x1, x3, x4, x)
f6(x1, x2, x3, x4, 0') → 0'
f5(x1, x2, x3, x4, 0') → 0'
f4(0', x2, x3, x4, x5) → 0'
f3(x1, x2, x3, x4, 0') → 0'
f2(x1, x2, 0', x4, x5) → 0'
f1(x1, x2, x3, x4, 0') → 0'
f0(x1, 0', x3, x4, x5) → 0'

Types:
f4 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
S :: S:0' → S:0'
f2 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
0' :: S:0'
f3 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
f5 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
f0 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
f1 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
f6 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
hole_S:0'1_7 :: S:0'
gen_S:0'2_7 :: Nat → S:0'

Generator Equations:
gen_S:0'2_7(0) ⇔ 0'
gen_S:0'2_7(+(x, 1)) ⇔ S(gen_S:0'2_7(x))

The following defined symbols remain to be analysed:
f3, f4

They will be analysed ascendingly in the following order:
f4 = f2
f4 = f3
f4 = f5
f4 = f0
f4 = f1
f4 = f6
f2 = f3
f2 = f5
f2 = f0
f2 = f1
f2 = f6
f3 = f5
f3 = f0
f3 = f1
f3 = f6
f5 = f0
f5 = f1
f5 = f6
f0 = f1
f0 = f6
f1 = f6

(19) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol f3.

(20) Obligation:

Innermost TRS:
Rules:
f4(S(x''), S(x'), x3, x4, S(x)) → f2(S(x''), x', x3, x4, x)
f4(S(x'), 0', x3, x4, S(x)) → f3(x', 0', x3, x4, x)
f2(x1, x2, S(x''), S(x'), S(x)) → f5(x1, x2, S(x''), x', x)
f2(x1, x2, S(x'), 0', S(x)) → f3(x1, x2, x', 0', x)
f4(S(x'), S(x), x3, x4, 0') → 0'
f4(S(x), 0', x3, x4, 0') → 0'
f2(x1, x2, S(x'), S(x), 0') → 0'
f2(x1, x2, S(x), 0', 0') → 0'
f0(x1, S(x'), x3, S(x), x5) → f1(x', S(x'), x, S(x), S(x))
f0(x1, S(x), x3, 0', x5) → 0'
f6(x1, x2, x3, x4, S(x)) → f0(x1, x2, x4, x3, x)
f5(x1, x2, x3, x4, S(x)) → f6(x2, x1, x3, x4, x)
f3(x1, x2, x3, x4, S(x)) → f4(x1, x2, x4, x3, x)
f1(x1, x2, x3, x4, S(x)) → f2(x2, x1, x3, x4, x)
f6(x1, x2, x3, x4, 0') → 0'
f5(x1, x2, x3, x4, 0') → 0'
f4(0', x2, x3, x4, x5) → 0'
f3(x1, x2, x3, x4, 0') → 0'
f2(x1, x2, 0', x4, x5) → 0'
f1(x1, x2, x3, x4, 0') → 0'
f0(x1, 0', x3, x4, x5) → 0'

Types:
f4 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
S :: S:0' → S:0'
f2 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
0' :: S:0'
f3 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
f5 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
f0 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
f1 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
f6 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
hole_S:0'1_7 :: S:0'
gen_S:0'2_7 :: Nat → S:0'

Generator Equations:
gen_S:0'2_7(0) ⇔ 0'
gen_S:0'2_7(+(x, 1)) ⇔ S(gen_S:0'2_7(x))

The following defined symbols remain to be analysed:
f4

They will be analysed ascendingly in the following order:
f4 = f2
f4 = f3
f4 = f5
f4 = f0
f4 = f1
f4 = f6
f2 = f3
f2 = f5
f2 = f0
f2 = f1
f2 = f6
f3 = f5
f3 = f0
f3 = f1
f3 = f6
f5 = f0
f5 = f1
f5 = f6
f0 = f1
f0 = f6
f1 = f6

(21) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol f4.

(22) Obligation:

Innermost TRS:
Rules:
f4(S(x''), S(x'), x3, x4, S(x)) → f2(S(x''), x', x3, x4, x)
f4(S(x'), 0', x3, x4, S(x)) → f3(x', 0', x3, x4, x)
f2(x1, x2, S(x''), S(x'), S(x)) → f5(x1, x2, S(x''), x', x)
f2(x1, x2, S(x'), 0', S(x)) → f3(x1, x2, x', 0', x)
f4(S(x'), S(x), x3, x4, 0') → 0'
f4(S(x), 0', x3, x4, 0') → 0'
f2(x1, x2, S(x'), S(x), 0') → 0'
f2(x1, x2, S(x), 0', 0') → 0'
f0(x1, S(x'), x3, S(x), x5) → f1(x', S(x'), x, S(x), S(x))
f0(x1, S(x), x3, 0', x5) → 0'
f6(x1, x2, x3, x4, S(x)) → f0(x1, x2, x4, x3, x)
f5(x1, x2, x3, x4, S(x)) → f6(x2, x1, x3, x4, x)
f3(x1, x2, x3, x4, S(x)) → f4(x1, x2, x4, x3, x)
f1(x1, x2, x3, x4, S(x)) → f2(x2, x1, x3, x4, x)
f6(x1, x2, x3, x4, 0') → 0'
f5(x1, x2, x3, x4, 0') → 0'
f4(0', x2, x3, x4, x5) → 0'
f3(x1, x2, x3, x4, 0') → 0'
f2(x1, x2, 0', x4, x5) → 0'
f1(x1, x2, x3, x4, 0') → 0'
f0(x1, 0', x3, x4, x5) → 0'

Types:
f4 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
S :: S:0' → S:0'
f2 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
0' :: S:0'
f3 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
f5 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
f0 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
f1 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
f6 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
hole_S:0'1_7 :: S:0'
gen_S:0'2_7 :: Nat → S:0'

Generator Equations:
gen_S:0'2_7(0) ⇔ 0'
gen_S:0'2_7(+(x, 1)) ⇔ S(gen_S:0'2_7(x))

No more defined symbols left to analyse.